(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^2).
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(x, s(y)) → if(le(x, s(y)), 0, p(minus(x, p(s(y)))))
if(true, x, y) → x
if(false, x, y) → y
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, 0) → z0
minus(z0, s(z1)) → if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Tuples:
P(0) → c
P(s(z0)) → c1
LE(0, z0) → c2
LE(s(z0), 0) → c3
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, 0) → c5
MINUS(z0, s(z1)) → c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
IF(true, z0, z1) → c7
IF(false, z0, z1) → c8
S tuples:
P(0) → c
P(s(z0)) → c1
LE(0, z0) → c2
LE(s(z0), 0) → c3
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, 0) → c5
MINUS(z0, s(z1)) → c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
IF(true, z0, z1) → c7
IF(false, z0, z1) → c8
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
P, LE, MINUS, IF
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 7 trailing nodes:
P(0) → c
LE(s(z0), 0) → c3
IF(true, z0, z1) → c7
LE(0, z0) → c2
IF(false, z0, z1) → c8
MINUS(z0, 0) → c5
P(s(z0)) → c1
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, 0) → z0
minus(z0, s(z1)) → if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, 0) → z0
minus(z0, s(z1)) → if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(LE(z0, s(z1)), MINUS(z0, p(s(z1))))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(LE(z0, s(z1)), MINUS(z0, p(s(z1))))
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(7) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
p(0) → 0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, 0) → z0
minus(z0, s(z1)) → if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(s(z0)) → z0
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(LE(z0, s(z1)), MINUS(z0, p(s(z1))))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, s(z1)) → c6(LE(z0, s(z1)), MINUS(z0, p(s(z1))))
K tuples:none
Defined Rule Symbols:
p
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MINUS(
z0,
s(
z1)) →
c6(
LE(
z0,
s(
z1)),
MINUS(
z0,
p(
s(
z1)))) by
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(s(z0)) → z0
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
K tuples:none
Defined Rule Symbols:
p
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(11) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
p(s(z0)) → z0
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
We considered the (Usable) Rules:none
And the Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(LE(x1, x2)) = 0
POL(MINUS(x1, x2)) = x2
POL(c4(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(s(x1)) = [1] + x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
K tuples:
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
Defined Rule Symbols:none
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
LE(s(z0), s(z1)) → c4(LE(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(LE(x1, x2)) = x1
POL(MINUS(x1, x2)) = x1·x2
POL(c4(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(s(x1)) = [1] + x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
S tuples:none
K tuples:
MINUS(x0, s(z0)) → c6(LE(x0, s(z0)), MINUS(x0, z0))
LE(s(z0), s(z1)) → c4(LE(z0, z1))
Defined Rule Symbols:none
Defined Pair Symbols:
LE, MINUS
Compound Symbols:
c4, c6
(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(18) BOUNDS(1, 1)